/**
 * Copyright (c) 2010 by Kevin Bierhoff.
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *    1. Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *    2. Redistributions in binary form must reproduce the above copyright
 *       notice, this list of conditions and the following disclaimer in the
 *       documentation and/or other materials provided with the distribution.
 *    3. Neither the names of the authors nor the
 *       names of its contributors may be used to endorse or promote products
 *       derived from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE AUTHORS ''AS IS'' AND ANY
 * EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
 * WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY
 * DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
 * INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
 * LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
 * ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
 * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 */
package com.googlecode.syper.javasyp.checker;

import java.util.ArrayList;
import java.util.Collections;
import java.util.Iterator;
import java.util.List;

import org.eclipse.jdt.core.dom.ASTNode;
import org.eclipse.jdt.core.dom.ArrayAccess;
import org.eclipse.jdt.core.dom.Expression;
import org.eclipse.jdt.core.dom.FieldAccess;
import org.eclipse.jdt.core.dom.IBinding;
import org.eclipse.jdt.core.dom.ITypeBinding;
import org.eclipse.jdt.core.dom.IVariableBinding;
import org.eclipse.jdt.core.dom.Name;
import org.eclipse.jdt.core.dom.SimpleName;
import org.eclipse.jdt.core.dom.ThisExpression;

/**
 * @author kevin
 *
 */
public final class PermInfo {

	// fixed in constructor
	private final PermKind perm;
	private final boolean consumable;
	private final boolean releasedWithFields;
	private final List<PermKind> dims;

	private final List<ASTNode> consumers = new ArrayList<ASTNode>();
	private final List<PermKind> consumed = new ArrayList<PermKind>();
	/** Only modify this set if not yet {@link #killed} */
	private final List<Object> disabled = new ArrayList<Object>();
	private boolean killed = false;
	// adding fields requires changes to copy constructor and mergeIn()

	public PermInfo(PermKind perm, boolean consumable, boolean releasedWithFields) {
		this(perm, consumable, releasedWithFields, Collections.<PermKind>emptyList());
	}

	public PermInfo(PermKind perm, boolean consumable, boolean releasedWithFields, List<PermKind> dims) {
		this.perm = perm;
		this.consumable = consumable;
		this.releasedWithFields = releasedWithFields;
		this.dims = dims;
	}

	/**
	 * Copy constructor to create a deep copy of the given object
	 * @param p {@code PermInfo} to copy
	 */
	PermInfo(PermInfo p) {
		this(p.perm, p.consumable, p.releasedWithFields, p.dims);
		this.consumers.addAll(p.consumers);
		this.consumed.addAll(p.consumed);
		this.disabled.addAll(p.disabled);
		this.killed = p.killed;
	}

	public PermKind getInitialPerm() {
		return perm;
	}

	public boolean isConsumable() {
		return consumable;
	}

	public boolean isReleasedWithFields() {
		return releasedWithFields;
	}

	public PermKind getEffectivePerm() {
		if (killed)
			return null;
		for (PermKind p : consumed) {
			switch (p) {
			case EXCL: return null;
			case IMM: return PermKind.IMM;
			default:
				throw new IllegalStateException("Unknown: " + p);
			}
		}
		return perm;
	}

	public List<? extends PermKind> getElemDims() {
		return dims;
	}

	public RefType getEffectiveType() {
		PermKind outer = getEffectivePerm();
		if (outer == null)
			return null;
		return ObjectType.getInstance(outer, ! consumable, false, getElemDims().toArray(new PermKind[0]));
	}

	/**
	 * Returns permission info for an array element accessed with the
	 * given expression <b>and updates the receiver permission to be consumed
	 * by the result</b>.
	 * @param consumer array access that should be associated with the returned info
	 * @return permission info for an array element accessed with the
	 * given expression
	 */
	public PermInfo accessArrayElement(ArrayAccess consumer) {
		if (dims.isEmpty() || dims.get(0) == null)
			// no permission for next dimension, don't consume this perm either
			return null;

		PermKind outer = getEffectivePerm();
		if (outer == null)
			// no permission for this array, no permission for next dimension available
			return null;

		PermKind elementPerm = outer.weaken(dims.get(0));
		if (elementPerm == null)
			throw new NullPointerException("unexpected null");

		try {
			consume(outer, consumer);
		} catch (PermissionException e) {
			throw new IllegalStateException("This should never fail", e);
		}

		PermInfo result = new PermInfo(
				elementPerm,
				false,
				false,
				dims.subList(1, dims.size()));
		result.addDisabled(consumer.getArray());
		return result;
	}

	public boolean isConsumed() {
		return ! consumers.isEmpty();
	}

	public void consume(PermKind consumed, ASTNode consumer) throws PermissionException {
		PermKind effPerm = getEffectivePerm();
		this.consumed.add(consumed);
		consumers.add(consumer);

		if (effPerm == null || ! effPerm.isStrongerThan(consumed))
			throw new PermissionException(
					// TODO include value description ("receiver", expression)
					"Need " + consumed + " but have " + (effPerm != null ? effPerm : "nothing"));
	}

	/**
	 * Convenience method to call either {@link #release(PermKind, ASTNode)}
	 * or {@link #release(PermKind, IVariableBinding)} depending on
	 * {@code consumer}'s type
	 * @param consumed
	 * @param consumer {@link ASTNode} or {@link IVariableBinding}
	 */
	public void release(PermKind consumed, Object consumer) {
		if (consumer instanceof IVariableBinding) {
			release(consumed, (IVariableBinding) consumer);
		} else {
			release(consumed, (ASTNode) consumer);
		}
	}

	public void release(PermKind consumed, ASTNode consumer) {
		// TODO use indexOf
		int index = consumers.lastIndexOf(consumer);
		if (index < 0)
			throw new IllegalStateException("Never consumed " + consumed
					+ " for " + consumer);
		this.consumed.remove(index);
		consumers.remove(index);
	}

	/**
	 * Release from assigned-to variable or field.
	 * @param consumed
	 * @param consumer variable binding of the assigned-to variable
	 */
	public void release(PermKind consumed, IVariableBinding consumer) {
		if (consumer.isEnumConstant())
			throw new IllegalArgumentException("Cannot release enum constants");
		consumer = consumer.getVariableDeclaration();
		// TODO use indexOf
		for (int i = consumers.size() - 1; 0 <= i; --i) {
			ASTNode n = consumers.get(i);
//			if (this.consumed.get(i) != consumed)
//				continue;
			if ((n instanceof SimpleName
					&& consumer.equals(((IVariableBinding) ((SimpleName) n).resolveBinding()).getVariableDeclaration()))
				|| (n instanceof FieldAccess
					&& ((FieldAccess) n).getExpression() instanceof ThisExpression
					&& consumer.equals(((FieldAccess) n).resolveFieldBinding().getVariableDeclaration()))) {
				this.consumed.remove(i);
				consumers.remove(i);
				return;
			}
		}
		throw new IllegalStateException("Never consumed " + consumed + " for "
				+ consumer);
	}

	/**
	 * Returns the permission consumed by the given consumer, if any
	 * @param consumer
	 * @return the permission consumed by the given consumer or {@code null}
	 */
	public PermKind getConsumed(Object consumer) {
		int index = indexOf(consumer);
		if (0 <= index)
			return consumed.get(index);
		else
			return null;
	}

	/**
	 * Returns the index of the given consumer in {@link #consumers} / {@link #consumed}
	 * @param consumer a {@link ASTNode} or {@link IVariableBinding}
	 * @return the index of the given consumer or -1 if not found
	 * @see List#indexOf(Object)
	 */
	private int indexOf(Object consumer) {
		if (consumer instanceof IVariableBinding) {
			consumer = ((IVariableBinding) consumer).getVariableDeclaration();
			for (int i = consumers.size() - 1; 0 <= i; --i) {
				ASTNode n = consumers.get(i);
				if ((n instanceof SimpleName
						&& consumer.equals(((IVariableBinding) ((SimpleName) n).resolveBinding()).getVariableDeclaration()))
					|| (n instanceof FieldAccess
						&& ((FieldAccess) n).getExpression() instanceof ThisExpression
						&& consumer.equals(((FieldAccess) n).resolveFieldBinding().getVariableDeclaration())))
					return i;
			}
			return -1;
		} else {
			return consumers.lastIndexOf(consumer);
		}
	}

	public void addDisabled(Expression newDisabled) {
		if (killed)
			throw new IllegalStateException("This permission is dead");
		disabled.add(newDisabled);
	}

	public void addDisabledReceiver(ITypeBinding receiver) {
		if (killed)
			throw new IllegalStateException("This permission is dead");
		disabled.add(receiver);
	}

	/**
	 * @param newEnabled
	 * @return {@code true} if {@code newEnabled} was disabled, {@code false} if not
	 */
	public boolean removeDisabled(Expression newEnabled) {
		if (killed)
			throw new IllegalStateException("This permission is dead");
		return disabled.remove(newEnabled);
	}

	/**
	 * Removes a disabled expression with the given variable binding, if any.
	 * @param var
	 * @return
	 */
	public boolean removeDisabled(IVariableBinding var) {
		if (killed)
			throw new IllegalStateException("This permission is dead");
		for (Iterator<Object> it = disabled.iterator(); it.hasNext(); ) {
			Object d = it.next();
			if (d instanceof Name) {
				IBinding binding = ((Name) d).resolveBinding();
				if (binding instanceof IVariableBinding
						&& var.equals(((IVariableBinding) binding).getVariableDeclaration())) {
					it.remove();
					return true;
				}
			}
		}
		return false;
	}

	/**
	 * Kills this permission, returning captured permissions that can be released.
	 * This method does not check whether the permission can be killed, which
	 * requires {@link #isConsumed()} to be {@code false} if there are no errors.
	 * @return captured permissions that can be released.
	 */
	// return as wildcard to avoid modification
	public List<?> kill() {
		if (killed)
			// disabled can be non-empty from mergeIn's
			return Collections.emptyList();
		killed = true;
		List<Object> result = new ArrayList<Object>(disabled);
		disabled.clear();
		return result;
	}

	// return as wildcard to avoid modification
	public List<? extends ASTNode> getConsumers() {
		return consumers;
	}

	public boolean isConsumableBy(List<? extends PermKind> elemDims) {
		if (dims.size() < elemDims.size())
			return false;
		for (int i = 0; i < elemDims.size(); ++i) {
			if (! dims.get(i).isStrongerThan(elemDims.get(i)))
				return false;
		}
		return true;
	}

	public void mergeIn(PermInfo other) {
		if (this.perm != other.perm ||
				this.consumable != other.consumable ||
				this.releasedWithFields != other.releasedWithFields ||
				! this.dims.equals(other.dims))
			throw new IllegalArgumentException();

		int i = 0;
		// find end of common prefix
		for ( ; i < this.consumers.size() && i < other.consumers.size() &&
				this.consumers.get(i) == other.consumers.get(i) &&
				this.consumed.get(i) == other.consumed.get(i); ++i)
			;
		// tack on extra consumers
		for ( ; i < other.consumers.size(); ++i) {
			this.consumers.add(other.consumers.get(i));
			this.consumed.add(other.consumed.get(i));
		}

		// find end of common prefix
		i = 0;
		for ( ; i < this.disabled.size() && i < other.disabled.size() &&
				this.disabled.get(i) == other.disabled.get(i); ++i)
			;
		// tack on extra disabled
		for ( ; i < other.disabled.size(); ++i)
			this.disabled.add(other.disabled.get(i));

		// assume killed if one of them is killed
		this.killed |= other.killed;
	}

	@Override
	public String toString() {
		StringBuilder result = new StringBuilder();
		if (killed)
			result.append("RELEASED: ");
		result.append(perm).append(disabled).append('\\').append(consumed);
		return result.toString();
	}
}
